Lambda the Ultimate

I found an interesting new paper by Edwin Brady.

Abstract. Dependent type theory has several practical applications in
the fields of theorem proving, program verifcation and programming
language design. Ivor is a Haskell library designed to allow easy extend-
ing and embedding of a type theory based theorem prover in a Haskell
application. In this paper, I give an overview of the library and show
how it can be used to implement formal systems such as propositional
logic. Furthermore, I sketch an implementation of a simple functional
programming language using the library; by using type theory as a core
representation, we can construct and evaluate terms and prove correct-
ness properties of those terms within the same framework, ensuring con-
sistency of the implementation and the theorem prover.

A report on Gilad Bracha's presentation at Lang.NET 2006 entitled "Dynamically Typed Languages on the Java Platform".

We discussed several of the ideas mentioned, but I think we should continue to follow this story.

Software Extension and Integration with Type Classes. Ralf Lämmel and Klaus Ostermann.

The abilities to extend a software module and to integrate a software module into an existing software system without changing existing source code are fundamental challenges in software engineering and programming-language design. We show that these challenges can be tackled, at the level of language expressiveness, by using the language concept of type classes, as it is available in the functional programming language Haskell. A detailed comparison with related work shows that type classes provide a powerful framework in which solutions to known software extension and integration problems can be provided. We also pinpoint several limitations of type classes in this context.

We've had a number of papers lately with solutions to the expression problem and related extensibility challenges, using various techniques in various languages. Here's one exploring the expressiveness of Haskell's type classes.

It's extremely instructive to compare different approaches to these now-standard problems, and in fact I wonder whether this would make an ineresting approach to a programming languages survey course: In CS 3xx we explore and compare a number of programming languages by exploring idiomatic solutions to standard software engineering challenges.

The authors are looking for comments on this draft for a few more days.

As you can understand from the lack of new posts, I am extremely busy (and I do mean extremely).

I hope the LtU editorial team will find interesting new stuff to post until I manage to resurface...

Another year gone! What a year it has been: so many new ideas, members and occasional guests it will take a year to mention them all.

This year LtU traffic grew in an unprecedented way, and at some points along the way it seemed like we may be losing our collective identity. The LtU community was never a formal organization, of course: You are a member if you consider yourself one and contribute to the community in whatever way you find appropriate. Too many people stopping by to ask one question and leaving soon after can hurt the community. I am glad to say that the LtU community proved strong enough to handle the surge in new users, and indeed managed to persuade many of the newcomers to stay as regular members. Several prominent researchers in the field began posting here occasionally, without having to be invited. It is an honour having them among us, and I will of course try to get them to guest blog when I get the chance. It is quite fun to see that most interesting questions raised about new papers are answered by the authors or their graduate students.

The cordial nature of the LtU community, even if sometimes obscured by rants and bickering, managed to prevail and keep LtU a nice place to visit even as traffic increased and the number of new members signing up daily became astonishing.

From day one I saw LtU as a community. As such it is incredibly important to me that LtU is not just informative and has members with diverse backgrounds and skills, but is also friendly and helpful. I will not mention the specific members who always go out of their way to help when others raise questions or ask for assistance. We all know who you are. In my mind you are the gold members of the LtU community.

A new Lambda-year is about to begin, and it's great to feel certain that next year is going to be as instructive and challenging as the year just ending.

Onward and upward!

Generics as a Library. Oliveira, Hinze and Löh.

A generic function is a function that is defined on the structure of data types: with a single definition, we obtain a function that works for many data types. In contrast, an ad-hoc polymorphic function requires a separate implementation for each data type. Previous work by Hinze on lightweight generic programming has introduced techniques that allow the definition of generic functions directly in Haskell. A severe drawback of these approaches is that generic functions, once defined, cannot be extended with ad-hoc behaviour for new data types, precluding the design of a customizable generic programming library based on the se techniques. In this paper, we present a revised version of Hinze's Generics for the masses approach that overcomes this limitation. Using our new technique, writing a customizable generic programming library in Haskell 98 is possible.

Pushing forward the state of the generics art in Haskell 98. They also discuss the application of their technique to the expression problem.

(Thanks to Jacques Carette for pointing in this direction.)

I’ll jump to the conclusion first. For people like me, who are proficient in Perl and Java, Ruby is remarkably, perhaps irresistibly, attractive.

Tim Bray shares his experience with Ruby.

The main advanatges seem to be more readable code, that the language seems to encourage short methods, and the lovely comuunity. Sounds good to me...

Interface Automata
by Luca de Alfaro, Thomas A. Henzinger

Conventional type systems specify interfaces in terms of values and domains.
We present a light-weight formalism that captures the temporal aspects of software
component interfaces. Specifically, we use an automata-based language to capture both
input assumptions about the order in which the methods of a component are called,
and output guarantees about the order in which the component calls external methods.
The formalism supports automatic compatibility checks between interface models, and
thus constitutes a type system for component interaction. Unlike traditional uses of
automata, our formalism is based on an optimistic approach to composition, and on
an alternating approach to design refinement. According to the optimistic approach,
two components are compatible if there is some environment that can make them work
together. According to the alternating approach, one interface refines another if it
has weaker input assumptions, and stronger output guarantees. We show that these
notions have game-theoretic foundations that lead to efficient algorithms for checking
compatibility and refinement.

The idea of expressing order of message exchange as type is certainly not new (as anyone exposed to web service choreography hype can tell - oh, just kidding, of course the theory is much older). However, the specific approach looks interesting (not the least because of appealing to game semantics).

Lightweight Static Capabilitites

We describe a modular programming style that harnesses modern type systems to verify safety conditions in practical systems. This style has three ingredients:

1. A compact kernel of trust that is specific to the problem domain.
2. Unique names (capabilities) that confer rights and certify properties, so as to extend the trust from the kernel to the rest of the application.
3. Static (type) proxies for dynamic values.

We illustrate our approach using examples from the dependent-type literature, but our programs are written in Haskell and OCaml today, so our techniques are compatible with imperative code, native mutable arrays, and general recursion. The three ingredients of this programming style call for (1) an expressive core language, (2) higher-rank polymorphism, and (3) phantom types.

Pursuant to this thread about the membrane pattern in static languages from Mark Miller's excellent Ph.D. thesis. I don't yet know whether a solution is derivable from this work, but Mark was kind enough to point me to it, and Oleg seems to want to see it distributed, so here it is—Mark and/or Oleg, please let me know if this is premature.

From the "Whoa!" files:

Concoqtion: Mixing Indexed Types and Hindley-Milner Type Inference

This paper addresses the question of how to extend OCaml’s Hindley-Milner type system with types indexed by logical propositions and proofs of the Coq theorem prover, thereby providing an expressive and extensible mechanism for ensuring fine-grained program invariants. We propose adopting the approached used by Shao et al. for certified binaries. This approach maintains a phase distinction between the computational and logical languages, thereby limiting effects and non-termination to the computational language, and maintaining the decidability of the type system. The extension subsumes language features such as impredicative first-class (higher-rank) polymorphism and type operators, that are notoriously difficult to integrate with the Hindley-Milner style of type inference that is used in OCaml. We make the observation that these features can be more easily integrated with type inference if the inference algorithm is free to adapt the order in which it solves typing constraints to each program. To this end we define a novel “order-free” type inference algorithm. The key enabling technology is a graph representation of constraints and a constraint solver that performs Hindley-Milner inference with just three graph rewrite rules.

Another tough-to-categorize one: dependent types, the Curry-Howard Correspondence, logic programming, theorem provers as subsystems of compilers, implementation issues... it's all in here.

Update: A prototype implementation is available here, but it took a bit of Google-fu to find, and it's brand new, so be gentle.

Update II: The prototype implementation isn't buildable out of the box, and includes a complete copy of both the Coq and O'Caml distributions, presumably with patches etc. already applied. So it's clearly extremely early days yet. But this feels very timely to me, perhaps because I've just started using Coq within the past couple of weeks, and got my copy of Coq'Art and am enjoying it immensely.

Update III: It occurs to me that this might also relate to Vesa Karvonen's comment about type-indexed functions, which occurs in the thread on statically-typed capabilities, so there might be a connection between this front-page story and the front-page story on lightweight static capabilities. That thought makes me happy; I love it when concepts converge.